import Mathlib.Order.Defs.PartialOrder
import Mathlib.Order.Notation
import Mathlib.Tactic.ToAdditive

-- test that we can translate between structures, reordering the arguments of the fields
class SemilatticeInf (α : Type) extends PartialOrder α, Min α where
  le_inf : ∀ a b c : α, a ≤ b → a ≤ c → a ≤ b ⊓ c

class SemilatticeSup (α : Type) extends PartialOrder α, Max α where
  protected sup_le : ∀ a b c : α, a ≤ c → b ≤ c → a ⊔ b ≤ c

attribute [to_dual] SemilatticeInf
attribute [to_dual (reorder := 3 4 5)] SemilatticeSup.sup_le

@[to_dual]
lemma SemilatticeInf.le_inf' {α : Type} [SemilatticeInf α] (a b c : α) : a ≤ b → a ≤ c → a ≤ b ⊓ c :=
  SemilatticeInf.le_inf a b c

@[to_dual]
lemma SemilatticeSup.sup_le' {α : Type} [SemilatticeSup α] (a b c : α) : a ≤ c → b ≤ c → a ⊔ b ≤ c :=
  SemilatticeSup.sup_le a b c

structure Lattice (α : Type) extends SemilatticeInf α, SemilatticeSup α

attribute [to_dual existing] Lattice.toSemilatticeInf

-- we still cannot reorder arguments of arguments, so `SemilatticeInf.mk` is not tranlatable
/--
error: @[to_dual] failed. The translated value is not type correct. For help, see the docstring of `to_additive`, section `Troubleshooting`. Failed to add declaration
instSemilatticeSupOfForallLeForallMax:
Application type mismatch: The argument
  le_inf
has type
  ∀ (a b c : α), b ≤ a → c ≤ a → b ⊔ c ≤ a
but is expected to have type
  ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ b ≤ c
in the application
  { toPartialOrder := inst✝¹, toMax := inst✝, sup_le := le_inf }
-/
#guard_msgs in
@[to_dual]
instance {α : Type} [PartialOrder α] [Min α]
    (le_inf : ∀ a b c : α, a ≤ b → a ≤ c → a ≤ b ⊓ c) : SemilatticeInf α where
  le_inf


-- If the given `reorder` is the same as the autogenerated one, we get a linter warning:
/--
warning: `to_dual` correctly autogenerated the `(reorder := ...)` argument for le_imp_le.
You may remove the `(reorder := ...)` argument.

Note: This linter can be disabled with `set_option linter.translateReorder false`
-/
#guard_msgs in
@[to_dual self (reorder := a b)]
theorem le_imp_le {α : Type} [PartialOrder α] (a b : α) : a ≤ b → a ≤ b := id

-- The comparison on `reorder`s can see that `a b` is the same as `b a`:
/--
warning: `to_dual` correctly autogenerated the `(reorder := ...)` argument for le_imp_le'.
You may remove the `(reorder := ...)` argument.

Note: This linter can be disabled with `set_option linter.translateReorder false`
-/
#guard_msgs in
@[to_dual self (reorder := b a)]
theorem le_imp_le' {α : Type} [PartialOrder α] (a b : α) : a ≤ b → a ≤ b := id

-- It is possible to overwrite the autogenerated `reorder`:
/--
error: `to_dual` validation failed: expected
  ∀ {α : Type} (a : α) [inst : PartialOrder α] (b : α), b ≤ a → b ≤ a
but 'le_imp_le''' has type
  ∀ {α : Type} [inst : PartialOrder α] (a b : α), a ≤ b → a ≤ b
-/
#guard_msgs in
@[to_dual self (reorder := 2 3)]
theorem le_imp_le'' {α : Type} [PartialOrder α] (a b : α) : a ≤ b → a ≤ b := id

-- We can even overwrite it with the empty `reorder`:
/--
error: `to_dual` validation failed: expected
  ∀ {α : Type} [inst : PartialOrder α] (a b : α), b ≤ a → b ≤ a
but 'le_imp_le'''' has type
  ∀ {α : Type} [inst : PartialOrder α] (a b : α), a ≤ b → a ≤ b
-/
#guard_msgs in
@[to_dual self (reorder := )]
theorem le_imp_le''' {α : Type} [PartialOrder α] (a b : α) : a ≤ b → a ≤ b := id

-- Test a larger permutation:

theorem refl₁ (a b c d e : Nat) : a + b + c + d + e = a + b + c + d + e := rfl

@[to_dual existing refl₁]
theorem refl₂ (b c a e d : Nat) : a + b + c + d + e = a + b + c + d + e := rfl

/-
TODO: If we tag something with `@[to_dual self]` and if there is no reorder, then this is useless.
So, we should have a linter warning about this.
The only exception is if we want to influence the tranlsation heuristic.
For example we tag `PUnit` with `@[to_dual self]`.
Maybe we should have a new command `@[to_dual_translate]`, analogous to `@[to_dual_dont_translate]`,
instead of using `@[to_dual self]` for those cases.
-/
@[to_dual self]
theorem not_lt_self {α : Type} [PartialOrder α] (a : α) : ¬ a < a := lt_irrefl a

-- Test that we do not translate numerals like we do in `@[to_additive]`
@[to_dual self]
theorem one_le_one {α : Type} [One α] [Preorder α] : (1 : α) ≤ 1 := le_rfl
